YES 1.306
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((elem :: Eq a => a -> [a] -> Bool) :: Eq a => a -> [a] -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((elem :: Eq a => a -> [a] -> Bool) :: Eq a => a -> [a] -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (elem :: Eq a => a -> [a] -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv2400), Succ(xv401000)) → new_primPlusNat(xv2400, xv401000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv2400), Succ(xv401000)) → new_primPlusNat(xv2400, xv401000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv3100), Succ(xv40100)) → new_primMulNat(xv3100, Succ(xv40100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv3100), Succ(xv40100)) → new_primMulNat(xv3100, Succ(xv40100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv300), Succ(xv4000)) → new_primEqNat(xv300, xv4000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv300), Succ(xv4000)) → new_primEqNat(xv300, xv4000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_@2, cc), cd), ce) → new_esEs(xv30, xv400, cc, cd)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, app(app(app(ty_@3, gg), gh), ha), ge) → new_esEs1(xv31, xv401, gg, gh, ha)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, eh, app(app(ty_Either, fh), ga)) → new_esEs2(xv32, xv402, fh, ga)
new_esEs3(:(xv30, xv31), :(xv400, xv401), app(ty_Maybe, bde)) → new_esEs0(xv30, xv400, bde)
new_esEs3(:(xv30, xv31), :(xv400, xv401), app(ty_[], bec)) → new_esEs3(xv30, xv400, bec)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, app(app(ty_@2, gc), gd), ge) → new_esEs(xv31, xv401, gc, gd)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(ty_Either, bac), bad), eh, ge) → new_esEs2(xv30, xv400, bac, bad)
new_esEs3(:(xv30, xv31), :(xv400, xv401), app(app(ty_@2, bdc), bdd)) → new_esEs(xv30, xv400, bdc, bdd)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, eh, app(ty_[], gb)) → new_esEs3(xv32, xv402, gb)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, app(ty_Maybe, gf), ge) → new_esEs0(xv31, xv401, gf)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, eh, app(app(app(ty_@3, fd), ff), fg)) → new_esEs1(xv32, xv402, fd, ff, fg)
new_esEs0(Just(xv30), Just(xv400), app(ty_Maybe, dh)) → new_esEs0(xv30, xv400, dh)
new_esEs2(Left(xv30), Left(xv400), app(app(ty_Either, bbe), bbf), bah) → new_esEs2(xv30, xv400, bbe, bbf)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), ba, app(ty_Maybe, bd)) → new_esEs0(xv31, xv401, bd)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, app(app(ty_Either, hb), hc), ge) → new_esEs2(xv31, xv401, hb, hc)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, eh, app(ty_Maybe, fc)) → new_esEs0(xv32, xv402, fc)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, eh, app(app(ty_@2, fa), fb)) → new_esEs(xv32, xv402, fa, fb)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(ty_[], bae), eh, ge) → new_esEs3(xv30, xv400, bae)
new_esEs3(:(xv30, xv31), :(xv400, xv401), bdb) → new_esEs3(xv31, xv401, bdb)
new_esEs2(Right(xv30), Right(xv400), bbh, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs1(xv30, xv400, bcd, bce, bcf)
new_esEs2(Left(xv30), Left(xv400), app(ty_[], bbg), bah) → new_esEs3(xv30, xv400, bbg)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), ba, app(app(app(ty_@3, be), bf), bg)) → new_esEs1(xv31, xv401, be, bf, bg)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(app(ty_@3, hh), baa), bab), eh, ge) → new_esEs1(xv30, xv400, hh, baa, bab)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, app(ty_[], hd), ge) → new_esEs3(xv31, xv401, hd)
new_esEs0(Just(xv30), Just(xv400), app(app(ty_@2, df), dg)) → new_esEs(xv30, xv400, df, dg)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(ty_Maybe, cf), ce) → new_esEs0(xv30, xv400, cf)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), ba, app(ty_[], cb)) → new_esEs3(xv31, xv401, cb)
new_esEs2(Left(xv30), Left(xv400), app(app(app(ty_@3, bbb), bbc), bbd), bah) → new_esEs1(xv30, xv400, bbb, bbc, bbd)
new_esEs0(Just(xv30), Just(xv400), app(ty_[], ef)) → new_esEs3(xv30, xv400, ef)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), ba, app(app(ty_Either, bh), ca)) → new_esEs2(xv31, xv401, bh, ca)
new_esEs2(Right(xv30), Right(xv400), bbh, app(app(ty_@2, bca), bcb)) → new_esEs(xv30, xv400, bca, bcb)
new_esEs2(Right(xv30), Right(xv400), bbh, app(app(ty_Either, bcg), bch)) → new_esEs2(xv30, xv400, bcg, bch)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), ba, app(app(ty_@2, bb), bc)) → new_esEs(xv31, xv401, bb, bc)
new_esEs2(Left(xv30), Left(xv400), app(app(ty_@2, baf), bag), bah) → new_esEs(xv30, xv400, baf, bag)
new_esEs2(Right(xv30), Right(xv400), bbh, app(ty_[], bda)) → new_esEs3(xv30, xv400, bda)
new_esEs3(:(xv30, xv31), :(xv400, xv401), app(app(ty_Either, bea), beb)) → new_esEs2(xv30, xv400, bea, beb)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_Either, dc), dd), ce) → new_esEs2(xv30, xv400, dc, dd)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(ty_Maybe, hg), eh, ge) → new_esEs0(xv30, xv400, hg)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(app(app(ty_@3, cg), da), db), ce) → new_esEs1(xv30, xv400, cg, da, db)
new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(ty_@2, he), hf), eh, ge) → new_esEs(xv30, xv400, he, hf)
new_esEs2(Left(xv30), Left(xv400), app(ty_Maybe, bba), bah) → new_esEs0(xv30, xv400, bba)
new_esEs2(Right(xv30), Right(xv400), bbh, app(ty_Maybe, bcc)) → new_esEs0(xv30, xv400, bcc)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(ty_[], de), ce) → new_esEs3(xv30, xv400, de)
new_esEs0(Just(xv30), Just(xv400), app(app(ty_Either, ed), ee)) → new_esEs2(xv30, xv400, ed, ee)
new_esEs0(Just(xv30), Just(xv400), app(app(app(ty_@3, ea), eb), ec)) → new_esEs1(xv30, xv400, ea, eb, ec)
new_esEs3(:(xv30, xv31), :(xv400, xv401), app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(xv30, xv400, bdf, bdg, bdh)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs3(:(xv30, xv31), :(xv400, xv401), app(app(ty_@2, bdc), bdd)) → new_esEs(xv30, xv400, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xv30), Just(xv400), app(app(ty_@2, df), dg)) → new_esEs(xv30, xv400, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(:(xv30, xv31), :(xv400, xv401), app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(xv30, xv400, bdf, bdg, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(xv30), Just(xv400), app(app(app(ty_@3, ea), eb), ec)) → new_esEs1(xv30, xv400, ea, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(xv30), Just(xv400), app(ty_[], ef)) → new_esEs3(xv30, xv400, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(:(xv30, xv31), :(xv400, xv401), app(ty_Maybe, bde)) → new_esEs0(xv30, xv400, bde)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(:(xv30, xv31), :(xv400, xv401), app(app(ty_Either, bea), beb)) → new_esEs2(xv30, xv400, bea, beb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xv30), Just(xv400), app(ty_Maybe, dh)) → new_esEs0(xv30, xv400, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(xv30), Just(xv400), app(app(ty_Either, ed), ee)) → new_esEs2(xv30, xv400, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_@2, cc), cd), ce) → new_esEs(xv30, xv400, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), ba, app(app(ty_@2, bb), bc)) → new_esEs(xv31, xv401, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), ba, app(app(app(ty_@3, be), bf), bg)) → new_esEs1(xv31, xv401, be, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(app(app(ty_@3, cg), da), db), ce) → new_esEs1(xv30, xv400, cg, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), ba, app(ty_[], cb)) → new_esEs3(xv31, xv401, cb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(ty_[], de), ce) → new_esEs3(xv30, xv400, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), ba, app(ty_Maybe, bd)) → new_esEs0(xv31, xv401, bd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(ty_Maybe, cf), ce) → new_esEs0(xv30, xv400, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), ba, app(app(ty_Either, bh), ca)) → new_esEs2(xv31, xv401, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_Either, dc), dd), ce) → new_esEs2(xv30, xv400, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, app(app(ty_@2, gc), gd), ge) → new_esEs(xv31, xv401, gc, gd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, eh, app(app(ty_@2, fa), fb)) → new_esEs(xv32, xv402, fa, fb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(ty_@2, he), hf), eh, ge) → new_esEs(xv30, xv400, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv30), Right(xv400), bbh, app(app(ty_@2, bca), bcb)) → new_esEs(xv30, xv400, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(xv30), Left(xv400), app(app(ty_@2, baf), bag), bah) → new_esEs(xv30, xv400, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, app(app(app(ty_@3, gg), gh), ha), ge) → new_esEs1(xv31, xv401, gg, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, eh, app(app(app(ty_@3, fd), ff), fg)) → new_esEs1(xv32, xv402, fd, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(app(ty_@3, hh), baa), bab), eh, ge) → new_esEs1(xv30, xv400, hh, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, eh, app(ty_[], gb)) → new_esEs3(xv32, xv402, gb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(ty_[], bae), eh, ge) → new_esEs3(xv30, xv400, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, app(ty_[], hd), ge) → new_esEs3(xv31, xv401, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, app(ty_Maybe, gf), ge) → new_esEs0(xv31, xv401, gf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, eh, app(ty_Maybe, fc)) → new_esEs0(xv32, xv402, fc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(ty_Maybe, hg), eh, ge) → new_esEs0(xv30, xv400, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, eh, app(app(ty_Either, fh), ga)) → new_esEs2(xv32, xv402, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(ty_Either, bac), bad), eh, ge) → new_esEs2(xv30, xv400, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), eg, app(app(ty_Either, hb), hc), ge) → new_esEs2(xv31, xv401, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Right(xv30), Right(xv400), bbh, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs1(xv30, xv400, bcd, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(Left(xv30), Left(xv400), app(app(app(ty_@3, bbb), bbc), bbd), bah) → new_esEs1(xv30, xv400, bbb, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(xv30), Left(xv400), app(ty_[], bbg), bah) → new_esEs3(xv30, xv400, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv30), Right(xv400), bbh, app(ty_[], bda)) → new_esEs3(xv30, xv400, bda)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(xv30), Left(xv400), app(ty_Maybe, bba), bah) → new_esEs0(xv30, xv400, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv30), Right(xv400), bbh, app(ty_Maybe, bcc)) → new_esEs0(xv30, xv400, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(xv30), Left(xv400), app(app(ty_Either, bbe), bbf), bah) → new_esEs2(xv30, xv400, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv30), Right(xv400), bbh, app(app(ty_Either, bcg), bch)) → new_esEs2(xv30, xv400, bcg, bch)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(:(xv30, xv31), :(xv400, xv401), app(ty_[], bec)) → new_esEs3(xv30, xv400, bec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(:(xv30, xv31), :(xv400, xv401), bdb) → new_esEs3(xv31, xv401, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3